
\begin{figure*}[t]
\begin{center}
\begin{tabular}{|c|}
\hline

$\typerule{
  \hl \not \in \dom(H)
    \gap
  \code{VI}' =
    \begin{cases}
    \Immut_\hl & \text{if~}\code{VI}=\Immut \text{~or~} (\code{VI}=\Immut_{\hc} \text{~and~} \hc \not \in K) \\
    \code{VI} & \text{otherwise} \\
    \end{cases}
}{
  K \vdash H,\code{new C<NO,VI>}\hparen{\ol{\hv}} \reducesto H[\hl \mapsto \code{C<NO,VI'>}\hparen{\ol{\code{null}}}],\hl\code{.build}\hparen{\ol{\hv}}\code{;return l}
}$~\RULE{(R-New)}\\\\


$\typerule{
  K \cup \{\hl\} \vdash H,\he \reducesto H',\code{e'}
}{
  K \vdash H,\code{e;return l} \reducesto H',\code{e';return l}
}$~\RULE{(R-c1)}
\quad
$\typerule{
  H[\hl] = \code{C<NO,NI>}\hparen{\ol{\hv}}
    \gap
  \fields{}(\hC)=\ol{\hf}
}{
  K \vdash H,\hl.\hf_i \reducesto H,\hv_i
}$~\RULE{(R-Field-Access)}\\\\

$\typerule{
  H[\hl] = \code{C<NO,NI>(}\ol{\hv}\code{)}
    \gap
  \fields{}(\hC)=\ol{\hf}
    \gap
  \code{NI}=\Mutable \text{~or~} \CookerH{\hl} \in K
    \gap
  \hv'=\code{null} \text{~or~} \hl \Oprec \OwnerH{\hv'}
}{
  K \vdash H,\hl.\hf_i = \hv' \reducesto H[\hl \mapsto \code{C<NO,NI>(}[\hv'/\hv_i]\ol{\hv}\code{)}],\hv'
}$~\RULE{(R-Field-Assignment)}\\\\


$\typerule{
}{
  K \vdash H,\code{v;return l} \reducesto H,\hl
}$~\RULE{(R-return)}
\quad
$\typerule{
  H[\hl] = \code{C<NO,NI>}\hparen{\ldots}
    \gap
  \mbody{}(\hm,\code{C})=\ol{\hx}.\he'
}{
  K \vdash H,\hl\code{.m(}\ol{\hv}\code{)} \reducesto H, [\ol{\hv}/\ol{\hx}, \hl/\this, \hl/\This, \code{NO}/\hO, \code{NI}/\hI]\he'
}$~\RULE{(R-Invoke)}\\


\hline
\end{tabular}
\end{center}
\caption{FOIGJ Reduction Rules ($K \vdash H,\he \reducesto H',\he'$), excluding all congruence rules except \RULE{R-c1}.} %(casting, field access, and method invocation are the same as in FJ)
\label{Figure:reduction}
\end{figure*}
